forall a: forall b: forall c:
forall Q:b->c:
O:a,b;Q = O:a,c